\begin{tabbing}
REF, NoConds
\\[0ex]on\_maybe\_hyp\=\{ABS:q, \$h:n\}\+
\\[0ex](${\it ident}$; ${\it tactic}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$OnHypMaybe (first\_nat \$h:n) ${\it ident}$ ($\backslash$h. ${\it tactic}$)$\cdot$
\end{tabbing}